Coq相关论文
由于信息技术的发展和国家政策的支持,各高校纷纷开始虚拟仿真实验教学平台的建设。但由于所建设的大部分实验教学平台搭载的实验......
近年来人工智能发展迅速,已经上升为国家级重大战略,夯实人工智能的基础理论尤为重要。数学定理的机器证明是人工智能基础理论研究......
核电站控制保护逻辑规模庞大、逻辑复杂,通常采用面向工程人员的图形语言开发,并自动生成C代码实现。如何保证图形语言到C代码转换......
在新一轮的技术变革中,人工智能是十分关键的推动因素,是当前科技发展的热点内容,该领域的重要分支之一就是定理机器证明,充分的融......
随着时代发展变革,计算机技术发展势如破竹,人工智能就是典型例证。机器定理证明是人工智能的重要内容,其起源可追至莱布尼茨时代,......
加快发展新一代人工智能是事关我国能否抓住新一轮科技革命和产业变革机遇的战略问题,定理证明作为人工智能领域的核心研究课题在......
布尔巴基学派的序、代数、拓扑三大母结构是现代数学的基础。利用交互式定理证明辅助工具Coq,可以完整构建这三大母结构的形式化系......
矩阵在理论数学、工程数学以及计算机科学中都有着广泛的应用。例如飞行控制系统的设计中,矩阵被用于飞行器受力状况的描述,运动学......
近年来人工智能发展迅速,已经上升为国家级重大战略,夯实人工智能的基础理论尤为重要。数学定理的机器证明是人工智能基础理论研究......
随着互联网的迅速发展和普及,网络数据流量越来愈庞大。企业信息化程度的不断加强,导致大量的数据亟待处理,数据已成为各类企业的......
学位
同步数据流语言在航空、高铁和核电等安全攸关领域得到了广泛的应用。其中基于一种类Lustre语言的Scade工具适合这些领域实时控制......
布尔巴基学派的序、代数、拓扑三大母结构是现代数学的基础.利用交互式定理证明工具Coq,可以完整构建这三大母结构的形式化系统.本......
PLC(可编程逻辑控制器)是一种嵌入式设备,广泛应用于工业控制领域。这些领域对程序的正确性要求很高,但传统的模拟、测试等方法无......
人工智能是一门研究模拟和延伸人的智能的一门新技术科学[1]。它作为计算机科学的一个分支,旨在了解智能的实质,并生产出一种新的......
工业控制系统的正确可靠对经济发展、人身安全和社会稳定有着重要意义。工业控制系统面对的一个基本问题是控制中的时序问题。如何......
随着互联网的飞速发展和软件开发的多样化,软件复杂性和需求量急剧增长。然而,伴随产生的软件质量与安全问题也日渐突出。近些年来......
本文基于证明辅助工具Coq,完整实现林群院士和张景中院士等倡导的第三代微积分—没有极限的微积分—理论构架的形式化验证,包括对......
实时操作系统常常运用优先级调度方案来进行抢占式调度.如果在这些操作系统中使用基于阻塞的同步原语则很容易产生无限优先级反转......
研究采用水培试验、盆栽试验和田间小区试验方法，通过对大豆叶片中辅酶Q_(10)（CoQ_(10)）含量、丙二醛（MDA）含量、大豆植株镁、铁、钠、......
The Unified Modeling Language (UML) is an industry standard for modeling analysis and design. However, the semantics of ......
同步语言具有确定性并行和精确时间语义等特性,因此被广泛用于设计和验证安全关键软件.随着安全关键领域应用多核处理器逐渐成为趋......
旨在建立CoQ高产菌株.通过ubiA基因和pkk223-3质粒构建重组质粒,双酶切和测序验证;发酵ubiA基因过表达菌株,分析CoQ产量和种类变化......
人工智能技术是国家目前重大科技发展战略之一,是计算机科学发展中非常重要的一个支系。随着现代社会计算机化、智能化程度的日渐......
人工智能是作为新一轮科技革命和产业变革的重要驱动力,是引领未来的战略性技术,已正式上升为国家战略。而人工智能中一个非常重要......
布拉霉菌菌丝体中分离提取辅酶Q，经硅胶柱和制备色谱纯化后纯度达98％。样品在Craven反应中显蓝色，紫外光谱扫描在275nm处有最大吸收，高......
通常情况下，我们很难确定一段给定的程序是否符合它的规范，程序提取是一种从构造性证明中提取函数式程序的机制，其构造特性很好地保证......
通常情况下，我们很难确定一段给定的程序是否符合它的规范，程序提取是一种从构造性证明中提取函数式程序的机制，其构造特性很好地保证......
基于计算机证明辅助工具Coq,参考“公理化集合论”形式化系统,实现朴素集合论形式化系统,并在此基础上给出有标集族及其交和并的形......
基于计算机证明辅助工具Coq,参考“公理化集合论”形式化系统,实现朴素集合论形式化系统,并在此基础上给出有标集族及其交和并的形......
同步数据流语言是一种广泛应用于核电及其他安全关键领域的语言,在同步数据流语言到顺序执行语言的翻译转换过程中,语义等价要保证......
同步数据流语言是一种广泛应用于核电及其他安全关键领域的语言,在同步数据流语言到顺序执行语言的翻译转换过程中,语义等价要保证......
矩阵在工程系统中有广泛的应用,矩阵运算的正确性对工程系统的可靠性有重要影响。Coq是一种基于带类型λ演算的功能强大的高阶定理......
矩阵在工程系统中有广泛的应用,矩阵运算的正确性对工程系统的可靠性有重要影响。Coq是一种基于带类型λ演算的功能强大的高阶定理......
随着软件运行时验证技术的发展,出现了许多面向C语言的运行时内存安全验证工具。这些工具大多是基于源代码或者中间代码插桩技术来......
Lustre是一种广泛应用于核电、航空等高可信领域的同步数据流语言。用形式化验证的方法来实现Lustre到C的翻译并证明其过程能有效......
使用定理证明器COQ验证和分析PLC抢答器程序的一些性质,证明了原程序的所有可能状态中只有半数是可达状态,揭示了系统在可达状态之......
SpaceOS是北京控制工程研究所自主研发的嵌入式实时操作系统,已被应用于探月工程、空间站等重大航天项目.SpaceOS作为底层系统软件......
Jourdan等在其2012年发表的论文“Validating LR(1)Parsers”中提出了一种形式化验证语法分析器的方法,并将其成功地应用于CompCer......
为确保星上操作系统中任务管理设计的可靠性,利用定理证明工具Coq对操作系统任务管理模块进行需求层建模及形式化验证.从用户角度,......
Paxos是一个在不可靠的分布式处理器网络中解决共识问题的算法族.共识问题是指分布式系统中一组参与者就一个结果达成一致的过程.......
随着人工智能技术的飞速发展,人工智能与数学领域的结合愈加密切,数学机械化的发展对数学领域与人工智能领域产生了深远影响。机器......
有限域GF(2n)是多种安全关键性算法的基础,包括AES加密算法、椭圆曲线加密和感染函数掩码等。相关资料表明,有限域上的运算因为自......
为解决实现同步数据流语言Lustre到串行命令式语言c语言可信编译器过程中碰到的时态运算翻译的困难，提出了将所有的时态运算翻译单......
从上世纪初到现在，质量管理从理论到实践都得到了较大的发展。现在许多企业都已经通过审核，建立起自己的质量管理体系，但是以质量成本......
